package edu.gatech.cc.concolic;

import edu.gatech.cc.concolic.expression.SymbolicExpression;
import gov.nasa.jpf.jvm.DynamicArea;
import gov.nasa.jpf.jvm.StackFrame;
import gov.nasa.jpf.jvm.bytecode.BALOAD;
import gov.nasa.jpf.jvm.bytecode.CALOAD;
import gov.nasa.jpf.jvm.bytecode.I2B;
import gov.nasa.jpf.jvm.bytecode.I2C;
import gov.nasa.jpf.jvm.bytecode.I2D;
import gov.nasa.jpf.jvm.bytecode.I2F;
import gov.nasa.jpf.jvm.bytecode.I2L;
import gov.nasa.jpf.jvm.bytecode.IADD;
import gov.nasa.jpf.jvm.bytecode.IALOAD;
import gov.nasa.jpf.jvm.bytecode.IAND;
import gov.nasa.jpf.jvm.bytecode.IDIV;
import gov.nasa.jpf.jvm.bytecode.IFEQ;
import gov.nasa.jpf.jvm.bytecode.IFGE;
import gov.nasa.jpf.jvm.bytecode.IFGT;
import gov.nasa.jpf.jvm.bytecode.IFLE;
import gov.nasa.jpf.jvm.bytecode.IFLT;
import gov.nasa.jpf.jvm.bytecode.IFNE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPGE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPGT;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPLE;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPLT;
import gov.nasa.jpf.jvm.bytecode.IF_ICMPNE;
import gov.nasa.jpf.jvm.bytecode.IINC;
import gov.nasa.jpf.jvm.bytecode.IMUL;
import gov.nasa.jpf.jvm.bytecode.INEG;
import gov.nasa.jpf.jvm.bytecode.IOR;
import gov.nasa.jpf.jvm.bytecode.IREM;
import gov.nasa.jpf.jvm.bytecode.ISHL;
import gov.nasa.jpf.jvm.bytecode.ISHR;
import gov.nasa.jpf.jvm.bytecode.ISUB;
import gov.nasa.jpf.jvm.bytecode.IUSHR;
import gov.nasa.jpf.jvm.bytecode.IXOR;
import gov.nasa.jpf.jvm.bytecode.L2D;
import gov.nasa.jpf.jvm.bytecode.L2F;
import gov.nasa.jpf.jvm.bytecode.L2I;
import gov.nasa.jpf.jvm.bytecode.LADD;
import gov.nasa.jpf.jvm.bytecode.LALOAD;
import gov.nasa.jpf.jvm.bytecode.LAND;
import gov.nasa.jpf.jvm.bytecode.LCMP;
import gov.nasa.jpf.jvm.bytecode.LDIV;
import gov.nasa.jpf.jvm.bytecode.LMUL;
import gov.nasa.jpf.jvm.bytecode.LNEG;
import gov.nasa.jpf.jvm.bytecode.LOOKUPSWITCH;
import gov.nasa.jpf.jvm.bytecode.LOR;
import gov.nasa.jpf.jvm.bytecode.LREM;
import gov.nasa.jpf.jvm.bytecode.LSHL;
import gov.nasa.jpf.jvm.bytecode.LSHR;
import gov.nasa.jpf.jvm.bytecode.LSUB;
import gov.nasa.jpf.jvm.bytecode.LUSHR;
import gov.nasa.jpf.jvm.bytecode.LXOR;
import gov.nasa.jpf.jvm.bytecode.TABLESWITCH;

public interface ExecutionStrategy {

	public SymbolicExpression makeSymbolic(int x);
	public SymbolicExpression makeSymbolic(char c);
		
	public Object execute(IADD insn, StackFrame sf);
	public Object execute(ISUB insn, StackFrame sf);
	public Object execute(IMUL insn, StackFrame sf);
	public Object execute(IDIV insn, StackFrame sf);
	public Object execute(IREM insn, StackFrame sf);
	//TODO: remove index and increment arguments when IINC has public getters
	public Object execute(IINC insn, StackFrame sf, int index, int increment);
	public Object execute(INEG insn, StackFrame sf);
	
	public Object execute(IAND insn, StackFrame sf);
	public Object execute(IOR insn, StackFrame sf);
	public Object execute(IXOR insn, StackFrame sf);
	
	public Object execute(ISHL insn, StackFrame sf);
	public Object execute(ISHR insn, StackFrame sf);
	public Object execute(IUSHR insn, StackFrame sf);
	
	public Object execute(I2B insn, StackFrame sf);
	public Object execute(I2C insn, StackFrame sf);
	public Object execute(I2D insn, StackFrame sf);
	public Object execute(I2F insn, StackFrame sf);
	public Object execute(I2L insn, StackFrame sf);
	public Object execute(L2D insn, StackFrame sf);
	public Object execute(L2F insn, StackFrame sf);
	public Object execute(L2I insn, StackFrame sf);
	
	public void execute(IF_ICMPEQ insn, StackFrame sf);
	public void execute(IF_ICMPNE insn, StackFrame sf);
	public void execute(IF_ICMPGE insn, StackFrame sf);
	public void execute(IF_ICMPGT insn, StackFrame sf);
	public void execute(IF_ICMPLE insn, StackFrame sf);
	public void execute(IF_ICMPLT insn, StackFrame sf);
	
	public void execute(IFEQ insn, StackFrame sf);
	public void execute(IFNE insn, StackFrame sf);
	public void execute(IFGE insn, StackFrame sf);
	public void execute(IFGT insn, StackFrame sf);
	public void execute(IFLE insn, StackFrame sf);
	public void execute(IFLT insn, StackFrame sf);
	
	public void execute(LOOKUPSWITCH insn, StackFrame sf);
	public void execute(TABLESWITCH insn, StackFrame sf);

	public void execute(BALOAD insn, StackFrame sf, DynamicArea da);
	public void execute(CALOAD insn, StackFrame sf, DynamicArea da);
	public void execute(IALOAD insn, StackFrame sf, DynamicArea da);
	public void execute(LALOAD insn, StackFrame sf, DynamicArea da);
	
	public Object execute(LADD insn, StackFrame sf);
	public Object execute(LAND insn, StackFrame sf);
	public Object execute(LCMP insn, StackFrame sf);
	public Object execute(LDIV insn, StackFrame sf);
	public Object execute(LMUL insn, StackFrame sf);
	public Object execute(LNEG insn, StackFrame sf);
	public Object execute(LOR insn, StackFrame sf);
	public Object execute(LREM insn, StackFrame sf);
	public Object execute(LSUB insn, StackFrame sf);
	public Object execute(LXOR insn, StackFrame sf);
	public Object execute(LSHL insn, StackFrame sf);
	public Object execute(LSHR insn, StackFrame sf);
	public Object execute(LUSHR insn, StackFrame sf);

	public void execute(Exception execption);
	
	public void exit();
}
